Inference at * 1 
Iof proof for Lemma lt int eq true elim sqequal:



1. i : 
2. j : 
  (i <z j ~ tt)  (i < j) 

latex

 by D 0 

latex

 1: 

 1: 3. i <z j ~ tt
 1:   i < j
 2: .....wf..... NILNIL

 2:   (i <z j ~ tt)  Type
 .

Definitions

P  Q, t  T